이 프로젝트는 3D 형상 연산(교집합) 알고리즘을 Lean 4로 구현하고 형식 검증(Formal verification)을 거친 사례입니다. 개발자는 복잡한 1,000줄 이상의 AI 생성 코드를 직접 검토할 필요 없이, 사람이 작성한 93줄의 핵심 명세와 Lean 컴파일러의 검증 결과만 신뢰하면 됩니다. 이를 통해 AI가 작성한 방대한 양의 코드와 증명 과정을 블랙박스로 처리하면서도 소프트웨어의 수학적 정확성을 완벽하게 보장받을 수 있음을 보여줍니다.
AI 스타트업 프라마나 랩스(Pramaana Labs)가 대형 언어 모델(LLM)의 오류와 환각을 잡기 위해 수학적 '형식 검증(Formal verification)'을 도입합니다. 이를 통해 법률, 세무, 신약 개발 등 오류가 치명적인 분야에서 기업들이 안전하게 AI를 활용할 수 있도록 돕고자 합니다.
천재 수학자 테렌스 타오는 AI가 수학 연구에 역사상 처음으로 '분업'을 도입할 수 있다고 주장합니다. 기존의 수학자들은 문제 설정부터 검증, 논문 작성까지 모든 것을 혼자 해야 했지만, 형식 검증 등 AI 기술의 도움으로 대규모 팀 간의 전문적 협업이 가능해진다는 것입니다. 다만, 인간의 통찰력과 엄격한 검증이 뒷받침될 때만 AI가 온전한 잠재력을 발휘할 수 있다고 강조하며 수학 연구의 패러다임 전환을 예고했습니다.
최신 LLM들이 동시성 및 분산 시스템 명세 언어인 TLA+를 사용해 시스템을 모델링하는 역량을 평가한 연구 결과입니다. 연구진이 개발한 자동화 벤치마크 'SysMoBench'에 따르면, 최신 LLM들은 문법이나 기본 실행 단계에서는 거의 완벽한 점수를 기록했지만, 실제 코드와 모델이 일치하는지 검증하는 단계(46%)와 핵심 속성을 만족하는지 확인하는 단계(41%)에서는 대폭 실패했습니다. 이는 현재 AI가 시스템 코드의 실제 구조를 추상화해 정확한 형식 모델을 작성하기보다는, 학습 데이터에 존재하는 교과서적인 예제를 단순히 암기하여 재생산하는 한계를 명확히 보여줍니다.